package model.solver;

/**
 * Class for managing of minisat parameter.
 * @author stephane
 *
 */
public class MiniSatParameter extends SolverParameter {

	public static final int NOT_USED = -4;
	public static final int MIN_VERBOSITY = 0;
	public static final int MAX_VERBOSITY = 3;
	public static final double MIN_DECAY = 0;
	public static final double MAX_DECAY = 1;
	public static final double MIN_RND_FREQ = 0;
	public static final double MAX_RND_FREQ = 1;
	
	
	private boolean pre = false;
	private ParameterValue asymm = ParameterValue.NOT_USED;
	private ParameterValue  rcheck = ParameterValue.NOT_USED;
	private int grow = NOT_USED;
	private ParameterValue polarityMode = ParameterValue.NOT_USED;
	private double decay = (int)NOT_USED;
	private double rndfreq = (int)NOT_USED;
	private int verbosity = NOT_USED;

	public boolean isPre() {
		return pre;
	}

	public void setPre(boolean pre) {
		this.pre = pre;
	}

	
	public ParameterValue getAsymm() {
		return asymm;
	}

	/**
	 * currently not used
	 * @param asymm doesn't matter ^^
	 */
	public void setAsymm(ParameterValue asymm) {
		//this.asymm = asymm;
	}

	public ParameterValue getRcheck() {
		return rcheck;
	}

	public boolean setRcheck(ParameterValue rcheck) {
		if(rcheck == ParameterValue.RANDOM)
			return false;
		this.rcheck = rcheck;
		return true;
	}

	public int getGrow() {
		return grow;
	}

	public boolean setGrow(int grow) {
		if(grow != NOT_USED && grow <= 0)
			return false;
		
		this.grow = grow;
		return true;
	}

	public ParameterValue getPolarityMode() {
		return polarityMode;
	}

	public void setPolarityMode(ParameterValue polarityMode) {
		this.polarityMode = polarityMode;
	}

	public double getDecay() {
		return decay;
	}

	public boolean setDecay(double decay) {
		if(decay != NOT_USED && (decay > MAX_DECAY || decay < MIN_DECAY))
			return false;
	
		this.decay = decay;
		return true;
	}

	public double getRndfreq() {
		return rndfreq;
	}

	public boolean setRndfreq(double rndfreq) {
		if(rndfreq != NOT_USED && (rndfreq > MAX_DECAY || rndfreq < MIN_DECAY))
			return false;
	
		this.rndfreq = rndfreq;
		return true;
	
	}

	public int getVerbosity() {
		return verbosity;
	}

	public boolean setVerbosity(int verbosity) {
		if(verbosity != NOT_USED && (verbosity > MAX_VERBOSITY || verbosity < MIN_VERBOSITY))
			return false;
			
		this.verbosity = verbosity;
		return true;
	}

	public MiniSatParameter() {
		// TODO Auto-generated constructor stub
	}

	/**
	 * check if the parameters respect are coherent : like if the timeout is correct
	 * @return
	 */
	public boolean basicCheck(){
		if(!super.basicCheck())
			return false;
		
		if(rcheck == ParameterValue.RANDOM)
			return false;
	
		if(grow != NOT_USED && grow <= 0)
			return false;
		
		if(decay != NOT_USED && (decay > MAX_DECAY || decay < MIN_DECAY))
			return false;
	
		if(rndfreq != NOT_USED && (rndfreq > MAX_DECAY || rndfreq < MIN_DECAY))
			return false;
	
		if(verbosity != NOT_USED && (verbosity > MAX_VERBOSITY || verbosity < MIN_VERBOSITY))
			return false;
			
		return true;
	}

	/**
	 * return the number of parameter that will be add in the command line giving the current parameter
	 * @return
	 */
	public int getCommandLineNbParameterSup(){
		int nb = 1; //pre
		if(asymm != ParameterValue.NOT_USED)
			nb++;
		
		if(rcheck != ParameterValue.NOT_USED)
			nb++;
		
		if(grow != NOT_USED)
			nb++;
		
		if(polarityMode != ParameterValue.NOT_USED)
			nb++;
		
		if(decay != NOT_USED)
			nb++;
		
		if(rndfreq != NOT_USED)
			nb++;
		
		if(verbosity != NOT_USED)
			nb++;
		
		return nb;
	}
	
}
